Nuprl Lemma : alle-at2_wf
11,40
postcript
pdf
es
:ES,
i
,
x
,
y
:Id,
P
:(vartype(
i
;
x
)
vartype(
i
;
y
)
). @
i
always.
P
(
v1
,
v2
)
latex
Definitions
x
:
A
.
B
(
x
)
,
,
t
T
,
@
i
always.
P
(
x1
;
x2
)
,
x
(
s1
,
s2
)
,
x
.
t
(
x
)
,
x
(
s
)
Lemmas
alle-at
wf
,
es-when
wf
,
subtype
rel
self
,
es-vartype
wf
,
es-E
wf
,
Id
wf
,
es-loc
wf
,
event
system
wf
origin
es:ES, i, x, y:Id, P:(vartype(i;x)
vartype(i;y)
). @i always.P(v1,v2) 
es:ES, i, x, y:Id, P:(vartype(i;x)vartype(i;y)). @i always.P(v1,v2) x:A. B(x) T
x. t(x)